import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.List;

public class TeoremaProposicional {
	// =========================================================================
	/**
	 * Esta clase TeoremaProposicional transforma la cadena de entrada en un
	 * Arbol de tipo Nodo. La cadena codifica el Arbol como se indica en la
	 * gramatica.
	 * 
	 * String: el string que encapsula el arbol dado devuelve el nodo raiz del
	 * arbol dado
	 */

	// V: numero maximo de variables en la formula proposicional
	public static final int valores = 4; // <-- (1)
	public static boolean[] tValor = new boolean[valores];
	public static char c;
	
	static final char CONJUNCION = 'x';
	static final char DISYUNCION = '+';
	static final char NEGADO = '-';
	static final char CONDICIONAL = '>';
	static final char ABRIR_PARENTESIS = '(';
	static final char CERRAR_PARENTESIS = ')';
	
	
	public static Nodo parseo(BufferedReader inputLine) throws IOException,
			ExcepcionParseo {

		Nodo nodo1 = condicionParseo(inputLine);
		if (c == CONDICIONAL) {
			c = (char) inputLine.read();
			Nodo nodo2 = parseo(inputLine);
			return new NodoBinario(new Character(CONDICIONAL), nodo1, nodo2);
		} else {
			return nodo1;
		}
	}

	public static Nodo condicionParseo(BufferedReader inputLine)
			throws IOException, ExcepcionParseo {
		Nodo nodo1 = parseo2(inputLine);
		if (c == CONJUNCION) {
			c = (char) inputLine.read();
			Nodo nodo2 = condicionParseo(inputLine);
			return new NodoBinario(new Character(CONJUNCION), nodo1, nodo2);
		} else if (c == DISYUNCION) {
			c = (char) inputLine.read();
			Nodo nodo2 = condicionParseo(inputLine);
			return new NodoBinario(new Character(DISYUNCION), nodo1, nodo2);
		} else {
			return nodo1;
		}

	}

	public static Nodo parseo2(BufferedReader inputLine) throws IOException,
			ExcepcionParseo {
		Nodo nodo = null;
		if (c == NEGADO) {
			c = (char) inputLine.read();
			Nodo nodo1 = parseo2(inputLine);
			nodo = new NodoUnico(new Character(NEGADO), nodo1);
		} else {
			nodo = parseoAtomico(inputLine);
		}
		;

		return nodo;
	}

	public static Nodo parseoAtomico(BufferedReader inputLine)
			throws IOException, ExcepcionParseo {
		Nodo nodo1 = null;
		if (('0' <= c) && (c <= '9')) {
			nodo1 = new NodoHoja(new Character(c));
			c = (char) inputLine.read();
			return nodo1;
		} else {
			if (c == ABRIR_PARENTESIS) {
				c = (char) inputLine.read();
				nodo1 = parseo(inputLine);
				if (c == CERRAR_PARENTESIS) {
					c = (char) inputLine.read();
				} else {
					throw new ExcepcionParseo();
				}
				;
				return nodo1;
			}
			;
		}
		;
		throw new ExcepcionParseo();
	}

	// -------------------------------------------------------------------------
	/**
	 * 
	 * arbol: arbol a evaluar
	 * 
	 */

	public static boolean evaluacionArbol(Nodo arbol) throws EvalExcepcion {
		// ---------------------- Inicio Metodo Recursivo
		// --------------------------------
		if (arbol instanceof NodoHoja) {

			return tValor[((Character) (((NodoHoja) arbol).valor)).charValue() - 48];
		} else if (arbol instanceof NodoUnico) {
			return !(evaluacionArbol(((NodoUnico) arbol).izquierdo));
		} else if (arbol instanceof NodoBinario) {
			boolean izquierdo = evaluacionArbol(((NodoBinario) arbol).izquierdo);
			boolean derecho = evaluacionArbol(((NodoBinario) arbol).derecho);
			if (((Character) (((NodoBinario) arbol).valor)).charValue() == DISYUNCION) {
				return izquierdo || derecho;
			} else if (((Character) (((NodoBinario) arbol).valor)).charValue() == CONJUNCION) {
				return izquierdo && derecho;
			} else if (((Character) (((NodoBinario) arbol).valor)).charValue() == CONDICIONAL) {
				return (!izquierdo) || derecho;
			}
		}
		;
		throw new EvalExcepcion();
		// ---------------------- Fin metodo recursivo
		// -------------------------
	}

	public static void main(String[] args) throws IOException, ExcepcionParseo {
		boolean pregunta = true;
		boolean a = true;
		System.out
				.println("Ingresar una formula proporcional de acuerdo a la gramatica, por favor");
		System.out
				.println("Las variables estan representadas de la siguiente manera:");
		System.out.println("p=0 ; q=1 ; r=2 ; s=3");

		Nodo arbol = null;
		try {
			BufferedReader inputLine = new BufferedReader(
					new InputStreamReader(System.in));
			c = (char) inputLine.read();
			arbol = parseo(inputLine);
			if (c != '\n') {
				throw new ExcepcionParseo();
			}
			; // <--- (2)
		} catch (IOException e) {
			e.printStackTrace();
			System.out.println("IOException!");
		} catch (ExcepcionParseo pex) {
			System.out.println(pex.getMessage());
			return;
		}
		;

		// ------ (inicio 0)

		if (arbol != null) {
			System.out
					.println("\nParseo del arbol de la formula proposicional:\n"
							+ arbol);
			System.out.print("\nEs Una Tautologia? ");

			for (int i = 0; i < (int) Math.pow(2, valores); i++) {
				try {
					a = evaluacionArbol(arbol);
				} catch (EvalExcepcion evalex) {
					System.out.println(evalex.getMessage());
				}
				;
				if (!a) {
					pregunta = false;
					break;
				} else {
					for (int k = 0; k < valores; k++) {
						if (tValor[k]) {
							tValor[k] = false;
						} else {
							tValor[k] = true;
							break;
						}
					}
				}
			}
			;

			// --------------------------------------------------------

			if (pregunta) {
				System.out.println("Si.");
			} else {
				System.out.println("NO.\nLa asignacion de la falsedad es:\n");
				for (int k = 0; k < valores; k++) {
					System.out.print(k + "=" + tValor[k] + "; ");
				}
				;
				System.out.println();
			}
			// --------------------------------------------------------
		}

	}
}